CS 206 -- Recursive Programming and Proving

			   LISP Proofs using EKL
			     November 30, 1982


Here is an improved version of the LISP axioms at the end of the EKL manual.
The text below is the actual commands that are input to EKL to declare these
axioms, but (at LOTSB) you can read them in faster by giving the command

		      (get-proofs nlispax prf ekl bx)

which will read in the file BX:<EKL>NLISPAX.PRF.  In addition to the set of
axioms, the next few pages of this handout contain sever proofs that use them.


- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl (u v w) (type: |ground|) (sort: |listp|))

(decl (x y z) (type: |ground|) (sort: |sexp|))

(decl (xa ya za) (type: |ground|) (sort: |atom|))

(decl (a b c) (type: |ground|))

(decl (phi) (type: |ground→truthval|))

(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
 (prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info

(axiom |∀xa.sexp(xa)|)
(label simpinfo)

(axiom |∀u.sexp u|)
(label simpinfo)

(axiom |∀x u.listp x.u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ listp cdr u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ sexp car u|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp car x|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp cdr x|)
(label simpinfo)

(axiom |∀u.u=nil ≡ null u|)
(label simpinfo)
(axiom |∀u.nil=u ≡ null u|)
(label simpinfo)

(axiom |∀x y.sexp x.y|)
(label simpinfo)

(axiom |∀x y.¬atom x.y|)
(label simpinfo)

(axiom |∀x u.¬null x.u|)
(label simpinfo)

(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ (car u.cdr u=u)|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ (car x.cdr x=x)|)
(label simpinfo)

;;;induction

(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)

(decl pars (type: |ground*|))
(axiom
 |∀nilcase def.
   ∃fun. ∀pars x u.fun(nil,pars)=nilcase(pars)∧
                   fun(x.u,pars)=def(x,u,fun(u,pars),pars)|)
(label listinductiondef)

(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

(axiom
 |∀atomcase defsexp.
   ∃fun. ∀pars x y.(atom x ⊃ fun(x,pars)=atomcase(x,pars))∧
                   (fun(x.y,pars)=defsexp(x,y,fun(x,pars),fun(y,pars),pars))|)
(label sexpinductiondef)

;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

(decl list (type: |ground* → ground|) (syntype: constant))
(decl lst (type: |ground*|))
(axiom |∀x.listp(list(x))|)
(label simpinfo)

(axiom |∀x.list(x) = x.nil|)
(label simpinfo)

(axiom |∀lst.listp(list(lst))|)
(label simpinfo)

(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
(decl append (type: |ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (infixname: *) (bindingpower: 840))

(axiom |∀u v.listp(u*v)|)
(label simpinfo) (label listappend)

(axiom |∀x u v.nil*v=v∧(x.u)*v=x.(u*v)|)
(label appendef) (label simpinfo)

(axiom |∀u.u*nil=u|)
(label simpinfo)

(axiom |∀x v.(x.nil)*v=x.v|)
(label simpinfo)

(axiom |∀u v w.u*v*w=u*(v*w)|)
(label apprassoc)

(axiom |∀u v w.u*v*w=(u*v)*w|)
(label applassoc)

;;;map functions on lists

(axiom |∀phi x u.allp(phi,nil)∧
                 (if phi(x) then allp(phi,x.u)=allp(phi,u) else ¬allp(phi,x.u))|)
(label allpdef)

(axiom |∀phi x u.¬somep(phi,nil)∧
                 (if phi(x) then somep(phi,x.u)
			    else somep(phi,x.u)=somep(phi,u))|)
(label somepdef)

(axiom |∀fn x u.mapcar(fn,nil)=nil∧mapcar(fn,x.u)=fn(x).mapcar(fn,u)|)
(label mapcardef)

(decl (alist a0 a1 a2) (type: ground) (sort: alistp))
(axiom |∀alist. listp alist|)
(label simpinfo) 

(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp (xa.y).alist|)
(label mkalist)

(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

(axiom |∀x xa y alist.
         assoc(x,nil)=nil∧
         assoc(x,(xa.y).alist)=(if x=xa then xa.y else assoc(x,alist))|)
(label assocdef)

(axiom |∀x alist.sexp assoc(x,alist)|)
(label simpinfo)

(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

(axiom |∀x y u. ¬member(x,nil)∧member(x,y.u)=(x=y∨member(x,u))|)
(label memberdef)
;EKL axioms and proofs for permutation functions

(proof permut)

(decl rac (unaryname: rac) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))
 
(decl rdc (unaryname: rdc) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl snoc (type: |(ground⊗ground)→ground|) (syntype: constant))

(axiom |∀x u.rdc (x.u)=(if null u then nil else x.rdc u)|)
(label rdcdef)

(axiom |∀x u.rac (x.u)=(if null u then x else rac u)|)
(label racdef)

(define snoc |∀x u.snoc(x,u) = u * x.nil|)
(label snocdef)

(decl reverse (unaryname: reverse) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rev (type: |ground⊗ground→ground|) (syntype: constant))

(define reverse |∀u.reverse u = rev(u,nil)|)
(label reverserev)

(axiom |∀x u v.rev(nil,v)=v∧rev(x.u,v)=rev(u,x.v)|)
(label revdef) (label simpinfo)

(axiom |∀u v.rev(u,v)=reverse u*v|)
(label revprop)

(axiom |∀x u.reverse(nil)=nil∧reverse(x.u)=(reverse u)*(x.nil)|)
(label reversedef) (label simpinfo)

(axiom |∀u.listp reverse u|)
(label reverselist) (label simpinfo)

(axiom |∀x.reverse (x.nil)=x.nil|)
(label simpinfo)

(axiom |∀u.reverse reverse u = u|)
(label simpinfo)
(label reversereverse)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(label reverseappend)

(decl lcycle (unaryname: lcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rcycle (unaryname: rcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(define lcycle |∀u.lcycle(u)=if null u then nil else snoc(car u,cdr u)|)
(label lcycledef) (label simpinfo)

(define rcycle |∀u.rcycle(u)=if null u then nil else rac u . rdc u|)
(label rcycledef) (label simpinfo)
;facts on append
;associativity and termination of append

(proof append)

(decl newappend (type: |(ground⊗(ground*))→ground|) (syntype: constant)
  (infixname: **) (bindingpower: 840))

(axiom |∀x u v.nil**u=u∧(x.u)**v=x.(u**v)|)
(label appendef1)

;termination

(ue (phi |λu.∀v.listp (u**v)|) listinduction
    (use appendef1 (mode: t)) simpinfo)
;∀U V.LISTP U ** V
(label listappend1)

;you can now deduce associativity as follows:

(ue (phi |λu.((u**v)**w)=(u**(v**w))|) listinduction
    (use appendef1 (mode: always)) simpinfo listappend1)
;∀U.(U ** V) ** W=U ** (V ** W)
 
;the other nil property

(ue  (phi |λu.u**nil=u|) listinduction
     (use appendef1 (mode: always)) simpinfo listappend1)
;∀U.U ** NIL=U
;facts on reverse: these do the facts mentioned in our meeting for reverse

(proof reverse)

;remove reverse facts from simpinfo so we don't use it accidentally

(unlabel simpinfo reversereverse)
(unlabel simpinfo reverselist)

;termination

(ue (phi |λu.listp reverse u|) listinduction
    (use reversedef (mode: always)) simpinfo)
;∀U.LISTP REVERSE U
(label simpinfo)

;proof of reverseappend

(ue (phi |λu.(reverse (u*v) = reverse(v) * reverse(u))|) listinduction
    (use reversedef (mode: always)) simpinfo)
;(∀X U.REVERSE (U*V)=REVERSE V*REVERSE U⊃
;      REVERSE (U*V)*X.NIL=REVERSE V*REVERSE U*X.NIL)⊃
;(∀U.REVERSE (U*V)=REVERSE V*REVERSE U)
(label step1)

(assume |reverse (u*v)=reverse v*reverse u|)
(label ass)

(tci (ass) |reverse (u*v)*x.nil=reverse v*reverse u*x.nil|
     (use ass (mode: always)) simpinfo))
;REVERSE (U*V)=REVERSE V*REVERSE U⊃REVERSE (U*V)*X.NIL=REVERSE V*REVERSE U*X.NIL
(label step2)

(rw step1 (use step2) simpinfo)
;∀U.REVERSE (U*V)=REVERSE V*REVERSE U

;proof of reversereverse from reverseappend

(ue (phi |λu.reverse (reverse u) = u|) listinduction
    (use (reversedef reverseappend) (mode: always))
    simpinfo)
;∀U.REVERSE (REVERSE U)=U

;proof of reverserev

(ue (phi |λu.∀v.(rev(u,v)=(reverse(u))*v)|) 
    listinduction
    ((use (reversedef revdef) (mode: always))
     (use apprassoc (mode: always)))
    simpinfo)
;∀U V.REV(U,V)=REVERSE U*V
 
(trw permut#reverserev (use *) simpinfo)
;∀U.REVERSE U=REV(U,NIL)
;properties of rac,rdc,snoc,lcycle,rcycle
;the current set of axioms for permut and lispax can be found in lispax.cmd[ekl,jk]

(proof cprops)

(trw |∀x u.snoc(x,u)=reverse(x.reverse(u))|
     (use (snocdef reversedef) (mode: t))
     simpinfo)
;∀X U.SNOC(X,U)=REVERSE (X.REVERSE U)

(trw |∀x u.listp snoc(x,u)| (use * (mode: always)) simpinfo)
;∀X U.LISTP SNOC(X,U)
(label simpinfo)

(ue (phi |λu.rac (u*(x.nil)) = x|) listinduction
    (use racdef (mode: always))
    simpinfo)
;∀U.RAC (U*X.NIL)=X
(label racfact)

(ue (phi |λu.¬NULL U*X.NIL|) listinduction nil simpinfo)
;∀U.¬NULL U*X.NIL
(label simpinfo)

(ue (phi |λu.rdc (u*(x.nil)) = u|) listinduction
    (use rdcdef (mode: always))
    simpinfo)
;∀U.RDC (U*X.NIL)=U
(label rdcfact)

(ue (phi |λu.¬null u ⊃ listp rac u|) listinduction 
    (part 1 (use racdef (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃LISTP RAC U
(label simpinfo)

(ue (phi |λu.¬null u ⊃ listp rdc u|) listinduction 
    (part 1 (use rdcdef (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃LISTP RDC U
(label simpinfo)

(ue (phi |λu.¬null u ⊃ snoc(rac u, rdc u)=u|) listinduction
    (part 1 (use (snocdef racdef rdcdef) (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃SNOC(RAC U,RDC U)=U
(label snocfact)
 
(trw |¬null snoc(x,u)| (open snoc) simpinfo)
;¬NULL SNOC(X,U)
(label simpinfo)

(trw |∀u.listp rcycle u| (use rcycledef (mode: always)) simpinfo)
;∀U.LISTP RCYCLE U
(label simpinfo)

(trw |∀u.listp lcycle u| (use lcycledef (mode: always)) simpinfo)
;∀U.LISTP LCYCLE U
(label simpinfo)

(trw |rcycle lcycle u=u|
     (use (rcycledef lcycledef snocdef racfact rdcfact) (mode: always))
     simpinfo)
;RCYCLE (LCYCLE U)=U
 
(rw snocfact (open snoc) simpinfo)
;∀U.¬NULL U⊃RDC U*RAC U.NIL=U

(trw |(lcycle rcycle u)=u|
     (open rcycle lcycle snoc)
     * simpinfo)
;LCYCLE (RCYCLE U)=U